module Grammar

// http://semmle.com/ql-language-reference/syntax/grammar/

sig Script {
	import : set Import,
	declaration : set Declaration
}

sig Import {
	id : Id,
}

sig Id {}

// DECLARATION

abstract sig Declaration {}

sig ClasslessPredicate extends Declaration {
	params : set Parameter,
	term : Term + TermC
}

sig Parameter {
	id : Id,
	type : TypeReference
}

sig Class extends Declaration {
	id : Id,
	extend : lone TypeReference,
	member : Member	
}

sig FromWhereSelect extends Declaration {
	from : Id -> TypeReference,
	where : Term + TermC,
	select :  (Expression + ExpressionC) -> lone Id,
	order_by : Id
}
fact {
	FromWhereSelect.order_by in FromWhereSelect.from.TypeReference
	(Expression + ExpressionC).(FromWhereSelect.select) in FromWhereSelect.from.TypeReference
}

// TYPE REFERENCE

abstract sig TypeReference {}

sig ClassReference extends TypeReference { 	id : Id }

sig ColumnTypeReference extends TypeReference { id : Id }

sig PrimitiveTypeReference extends TypeReference {} // int | foat | string | boolean

// TERM

abstract sig TermC {}

sig not_Term extends TermC {
	not_term : Term + TermC
}

sig or_Term extends TermC {
	term1 : Term + TermC,
	term2 : Term + TermC
}

sig and_Term extends TermC {
	term1 : Term + TermC,
	term2 : Term + TermC
}

sig exists1_Term extends TermC {
	expr :  Expression + ExpressionC
}

sig exists2_Term extends TermC {
	term : Term + TermC,
	var_declaration : Id -> TypeReference
}

sig exists3_Term extends TermC {
	term1 : Term + TermC,
	term2 : Term + TermC,
	var_declaration : Id -> TypeReference
}

sig forall1_Term extends TermC {
	term : Term + TermC,
	var_declaration : Id -> TypeReference
}

sig forall2_Term extends TermC {
	term1 : Term + TermC,
	term2 : Term + TermC,
	var_declaration : Id -> TypeReference
}

sig forex_Term extends TermC {
	term1 : Term + TermC,
	term2 : Term + TermC,
	var_declaration : Id -> TypeReference
}

sig implies_Term extends TermC {
	term1 : Term + TermC,
	term2 : Term + TermC
}

sig if_then_else_Term extends TermC {
	if_term : Term + TermC,
	then_term : Term + TermC,
	else_term : Term + TermC
}

abstract sig Term extends TermC {}

sig Comp_Term extends Term {
	expr1 : Expression + ExpressionC,
	expr2 : Expression + ExpressionC,
	comparation_operator : CompOperator
}

sig CompOperator {}

sig instance_of_Term extends Term {
	expr : Expression + ExpressionC,
	instanceof : TypeReference
}

sig PredicateOrMethodCall_Term extends Term {
	expr1 : Expression + ExpressionC,
	expr2 : Expression + ExpressionC,
	id : Id
}

sig LiteralArgument extends Term {
	expr : Expression + ExpressionC
}

// MEMBER

abstract sig Member {}

sig Constructor extends Member {
	id : Id,
	term : Term + TermC
}

sig Predicate extends Member {
	id : Id,
	param : Parameter,
	term : Term + TermC
}

sig Method extends Member {
	type : TypeReference,
	id : Id,
	param : Parameter,
	term : Term + TermC
}


//EXPRESSSION

abstract sig ExpressionC {}

sig Unary_Expression extends ExpressionC {
	unary_operator : UnaryOperator,
	expr : Expression + ExpressionC
}

sig UnaryOperator {}

sig Binary_Expression extends ExpressionC {
	expr1 : Expression + ExpressionC,
	expr2 : Expression + ExpressionC,
	binary_operator : BinaryOperator
}

sig BinaryOperator {}

sig Type_Expression extends ExpressionC {
	type : TypeReference,
	expr : Expression + ExpressionC
}

abstract sig Expression extends ExpressionC {}

sig Constant extends Expression {} // true | false | int | float | string

sig Variable extends Expression {} // identifier | this | super | result

sig PredicateOrMethodCall_Expression extends Expression {
	expr1 : Expression + ExpressionC,
	expr2 : Expression + ExpressionC,
	id : Id
}

sig Agregate extends Expression {}

/*
import default

 //A class that defines an equals method but no hashCode method 
class EqNoHash extends Class {
  EqNoHash() {
    this.getAMethod() instanceof EqualsMethod and
		not this.getAMethod() instanceof HashCodeMethod and
    this.getSourceDeclaration().fromSource()
  }
}

// is e an expression in which t is used in a hashing data structure? 
predicate usedInHash(RefType t, Expr e) {
  exists(RefType s |
           s.getName().matches("%Hash%") and
           (   exists(MethodAccess ma | 
                        ma.getQualifier().getType() = s and
                        ma.getArgument(0).getType() = t and
                        e = ma) 
            or exists(ConstructorCall cc |
                        cc.getType() = s and
                        ((ParameterizedType)s).getTypeArgument(0) = t and
                        cc = e)))
}

from EqNoHash t, Expr e
where usedInHash(t, e)
select e, "Objects of this type are stored in hashing data structure, "
          + "but it does not have an explicit definition of hashCode()"


*/
pred HashedButNotHash [s:Script] {

	s.import = none
	one EqNoHash : Class {
		EqNoHash.extend in (one ClassReference)
		EqNoHash.member in Constructor
		(EqNoHash.member & Constructor).param = none
		EqNoHash.member.type = none
		(EqNoHash.member & Constructor).term in and_Term
		((EqNoHash.member & Constructor).term & and_Term).term1 in and_Term
		(((EqNoHash.member & Constructor).term & and_Term).term1  & and_Term).term1 in PredicateOrMethodCall_Term
		(((EqNoHash.member & Constructor).term & and_Term).term1  & and_Term).term2 in not_Term
		((EqNoHash.member & Constructor).term & and_Term).term2 in PredicateOrMethodCall_Term
	
	one usedInHash : ClasslessPredicate {
		usedInHash.params.type in ClassReference
		usedInHash.term in exists2_Term
		(usedInHash.term & exists2_Term).term in and_Term
		((usedInHash.term & exists2_Term).term & and_Term).term1 in PredicateOrMethodCall_Term
		((usedInHash.term & exists2_Term).term & and_Term).term2 in or_Term
		(((usedInHash.term & exists2_Term).term & and_Term).term2 & or_Term).term1 in exists2_Term
		(((usedInHash.term & exists2_Term).term & and_Term).term2 & or_Term).term2 in exists2_Term
		//(usedInHash.term & exists2_Term).var_declaration 		

	
	one fws : FromWhereSelect {
		one c : ClassReference | c.id = EqNoHash.id  => fws.from in ( Id -> c) 
		fws.where in PredicateOrMethodCall_Term
		fws.select in (Binary_Expression -> Id)
	
	s.declaration = EqNoHash + usedInHash + FromWhereSelect

	}
	}
	}
}

assert regra {
	not one s : Script | HashedButNotHash[s]
}

check regra for 8 but exactly 1 Script

run {}
